T:Type, R:(TTprop{i:l}).
(x:T. R(x,x))
 (x,y:T. R(x,y)  (R(y,x)))
 (as,bs:(T List).
 l-ordered(T; x,y.R(x,y); as)
  l-ordered(T; x,y.R(x,y); bs)
  ((as = bs)  (x:T. (x  as)  (x  bs)))) 

latex

Definitions	x,y. t(x;y), Type, no_repeats(T; l), s = t, type List, prop{i:l}, x:AB(x), x:A  B(x), (x  l), P  Q, left + right, f(a), P  Q, P  Q, x(s1,s2), P  Q, l_before(x; y; l; T), l-ordered(T; x,y.R(x;y); L), x:A. B(x), t  T, A, P  Q, False
Lemmas	l before member2, l before member, l tricotomy, l before wf, l member wf, iff wf, l-ordered-no repeats, no repeats-before-equality, not wf, l-ordered wf